COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	declare INDCONST S0 ε situation
C00004 ENDMK
C⊗;
declare INDCONST S0 ε situation;
declare INDCONST Robot Outside Table Box1 Box2 Door ε tower;
declare PREDCONST key(tower) [pre];
declare PREDCONST red(tower)[pre];
declare PREDCONST theseblocks tower;
extension theseblocks {Box1 Box2 Door Outside Robot Table};

axiom movable:
	∀t1 t2 s.(movable(t1,t2,s) ≡
(t1 = Robot ∧ (t2 = Box1 ∨ t2 = Box2 ∨ t2 = Door ∨ t2 = Table ∨ t2 = Outside)
	∧ (¬(t2 = Outside) ∨ ∃t.(key t ∧ on(t,Door,s))))
∨ (t2 = Robot ∧ ∀t4.¬on(t4,Robot,s) ∧
	∃t3.(on(Robot,t3,s) ∧ on(t1,t3,s)))
∨ (on(t1,Robot,s) ∧ on(Robot,t2,s)))
;;

axiom initial:
	∃t1 t2.(key t1 ∧ (t2 = Box1 ∨ t2 = Box2) ∧ on(t1,t2,S0)
		∧ ∀t3.(on(t3,t2,S0) ⊃ key t3 ∨ t3 = Robot))

	∃t1.(red t1 ∧ on(t1,Door,S0))

	∀t1.(on(t1,Door,S0) ⊃ red t1 ∨ t1 = Robot)

	∀t.(on(t,Table,S0) ⊃ t = Robot)

	∀t1 t2.(on(t1,Robot,S0) ∧ on(t2,Robot,S0) ⊃ t1 = t2)

	¬on(Robot,Outside,S0)
;;